
; Copyright (c) 2015 Microsoft Corporation
;; BUG: mpf != fpu [seed=1365428516, num_tests=3625]
;; sse2 FPU RM (before) : rm-up
;; sse2 FPU RM (after) : rm-up
;; Rounding mode: to positive
;; Precision: double (11/53)
;; X = -1.9850793959684056577685851152637042105197906494140625p826 {- 4436403200613665 826 (-8.88289e+248)}
;; Y = +1.723186192331428667756654249387793242931365966796875p-897 {+ 3256941066303310 -897 (1.6309e-270)}
;; Z = +1.3970652990759229172823552289628423750400543212890625p-273 {+ 1788223132960081 -273 (9.20509e-083)}
;; -1.9850793959684056577685851152637042105197906494140625p826 x +1.723186192331428667756654249387793242931365966796875p-897 +1.3970652990759229172823552289628423750400543212890625p-273 == -1.710330702907184363681381000787951052188873291015625p-70

;; mpf : - 3199045088922618 -70
;; mpfd: - 3199045088922618 -70 (-1.44871e-021) class: Neg. norm. non-zero
;; hwf : - 3199045088922619 -70 (-1.44871e-021) class: Neg. norm. non-zero

(set-logic QF_FP)
(set-info :status unsat)

(define-sort FPN () (_ FloatingPoint 11 53))
(declare-const x FPN)
(declare-const y FPN)
(declare-const z FPN)
(declare-const r FPN)
(declare-const q FPN)
(declare-const mpfx FPN)

(assert (= mpfx (fp.fma roundTowardPositive
		  ((_ to_fp 11 53) roundNearestTiesToEven (- 1.9850793959684056577685851152637042105197906494140625) 826)
		  ((_ to_fp 11 53) roundNearestTiesToEven 1.723186192331428667756654249387793242931365966796875 (- 897))
		  ((_ to_fp 11 53) roundNearestTiesToEven 1.3970652990759229172823552289628423750400543212890625 (- 273)))
	  ((_ to_fp 11 53) roundNearestTiesToEven (- 1.7103307029071845857259859258192591369152069091796875) (- 70))))


(assert (= x ((_ to_fp 11 53) roundNearestTiesToEven (- 1.9850793959684056577685851152637042105197906494140625) 826)))
(assert (= y ((_ to_fp 11 53) roundNearestTiesToEven 1.723186192331428667756654249387793242931365966796875 (- 897))))
(assert (= z ((_ to_fp 11 53) roundNearestTiesToEven 1.3970652990759229172823552289628423750400543212890625 (- 273))))

(assert (= r ((_ to_fp 11 53) roundNearestTiesToEven (- 1.7103307029071845857259859258192591369152069091796875) (- 70))))

(assert (= q (fp.fma roundTowardPositive x y z)))

(assert (not (= q r)))

(check-sat)
(check-sat-using smt)
